ac66108c920bcfd08dcea43c6357d5db72b9c612,OpenJML/src/org/jmlspecs/openjml/JmlTreeUtils.java,JmlTreeUtils,opType,#Type#Type#,596

Before Change


        if (lhs == types.REAL || rhs == types.REAL) return types.REAL;
        if (lhs == types.BIGINT || rhs == types.BIGINT) return types.BIGINT;
        if (lhs == types.TYPE || rhs == types.TYPE) return types.TYPE;
        if (TypeTag.INT.ordinal() >= lhsu.getTag().ordinal() && TypeTag.INT.ordinal() >= rhsu.getTag().ordinal()) return syms.intType;
        if (TypeTag.LONG.ordinal() >= lhsu.getTag().ordinal() && TypeTag.LONG.ordinal() >= rhsu.getTag().ordinal()) return syms.longType;
        if (TypeTag.DOUBLE.ordinal() >= lhsu.getTag().ordinal() && TypeTag.DOUBLE.ordinal() >= rhsu.getTag().ordinal()) return syms.doubleType;
        throw new JmlInternalError("Unknown combined type for " + lhs + " and " + rhs);
    }

After Change


        if (lhs == types.BIGINT || rhs == types.BIGINT) return types.BIGINT;
        if (lhs == types.TYPE || rhs == types.TYPE) return types.TYPE;
        TypeTag ltag = lhsu.getTag();
        TypeTag rtag = rhsu.getTag();
        
        if (ltag == TypeTag.DOUBLE) return lhs;
        if (rtag == TypeTag.DOUBLE) return rhs;